%% hal-00820871, version 1
%% http://hal.inria.fr/hal-00820871
@inproceedings{lucanu:hal-00820871,
    hal_id = {hal-00820871},
    url = {http://hal.inria.fr/hal-00820871},
    title = {{Program Equivalence by Circular Reasoning}},
    author = {Lucanu, Dorel and Rusu, Vlad},
    abstract = {{We propose a logic and a deductive system for stating and automatically proving the equivalence of programs in deterministic languages having a rewriting-based operational semantics. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that our approach is suitable for proving the equivalence of both terminating and non-terminating programs, and also the equivalence of both concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves in one shot the equivalence of (possibly, infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. We also report on a prototype implementation of the proposed deductive system in the K Framework.}},
    language = {Anglais},
    affiliation = {Department of Computer Science , DART - INRIA Lille - Nord Europe},
    booktitle = {{Integrated Formal Methods}},
    publisher = {Springer},
    address = {Turku, Finland},
    volume = {7940},
    series = {Lecture Notes in Computer Science },
    audience = {internationale },
    year = {2013},
    month = Jun,
    pdf = {http://hal.inria.fr/hal-00820871/PDF/ifm.pdf},
}

@inproceedings{DBLP:conf/rta/HillsR07,
  author    = {Mark Hills and
               Grigore Rosu},
  title     = {KOOL: An Application of Rewriting Logic to Language Prototyping
               and Analysis},
  booktitle = {RTA},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4533},
  year      = {2007},
  pages     = {246-256},
  ee        = {http://dx.doi.org/10.1007/978-3-540-73449-9_19}
}

@book{Baader:1998:TR:280474,
  author    = {Franz Baader and
               Tobias Nipkow},
  title     = {Term rewriting and all that},
  publisher = {Cambridge University Press},
  year      = {1998},
  isbn      = {978-0-521-45520-6},
  pages     = {I-XII, 1-301},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  address = {New York, NY, USA},
} 


@article{DBLP:journals/iandc/LynchV95,
  author    = {Nancy A. Lynch and
               Frits W. Vaandrager},
  title     = {Forward and Backward Simulations: {I.~Untimed} Systems},
  journal   = {Inf. Comput.},
  volume    = {121},
  number    = {2},
  year      = {1995},
  pages     = {214-233},
  ee        = {http://dx.doi.org/10.1006/inco.1995.1134},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Maude,
  author    = {Jos{\'e} Meseguer},
  title     = {Rewriting Logic and {Maude}: Concepts and Applications},
  booktitle = {RTA},
  year      = {2000},
  pages     = {1-26},
  ee        = {http://dx.doi.org/10.1007/10721975_1},
  crossref  = {DBLP:conf/rta/2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/rta/2000,
  editor    = {Leo Bachmair},
  title     = {Rewriting Techniques and Applications, 11th International
               Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings},
  booktitle = {RTA},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1833},
  year      = {2000},
  isbn      = {3-540-67778-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/tacas/MouraB08,
  author    = {Leonardo Mendon\c{c}a de Moura and
               Nikolaj Bj{\o}rner},
  title     = {Z3: An Efficient {SMT} Solver},
  booktitle = {TACAS},
  year      = {2008},
  pages     = {337-340},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78800-3_24},
  crossref  = {DBLP:conf/tacas/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2008,
  editor    = {C. R. Ramakrishnan and
               Jakob Rehof},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 14th International Conference, TACAS 2008, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2008, Budapest, Hungary, March
               29-April 6, 2008. Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4963},
  year      = {2008},
  isbn      = {978-3-540-78799-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/iandc/SerbanutaRM09,
  author    = {Traian-Florin {\c S}erb{\u a}nu{\c t}{\u a} and
               Grigore Ro{\c s}u and
               Jos{\'e} Meseguer},
  title     = {A rewriting logic approach to operational semantics},
  journal   = {Inf. Comput.},
  volume    = {207},
  number    = {2},
  year      = {2009},
  pages     = {305-340},
  ee        = {http://dx.doi.org/10.1016/j.ic.2008.03.026},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{DBLP:journals/entcs/EscobarMS09,
  author    = {Santiago Escobar and
               Jos{\'e} Meseguer and
               Ralf Sasse},
  title     = {Variant Narrowing and Equational Unification},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {238},
  number    = {3},
  year      = {2009},
  pages     = {103-119},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2009.05.015},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/lisp/MeseguerT07,
  author    = {Jos{\'e} Meseguer and
               Prasanna Thati},
  title     = {Symbolic reachability analysis using narrowing and its application
               to verification of cryptographic protocols},
  journal   = {Higher-Order and Symbolic Computation},
  volume    = {20},
  number    = {1-2},
  year      = {2007},
  pages     = {123-160},
  ee        = {http://dx.doi.org/10.1007/s10990-007-9000-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{rosu-stefanescu-2012-oopsla,
  author    = {Grigore Ro{\c s}u and
               Andrei {\c S}tef{\u a}nescu},
  title     = {Checking reachability using matching logic},
  booktitle = {OOPSLA},
  year      = {2012},
  pages     = {555-574},
  ee        = {http://doi.acm.org/10.1145/2384616.2384656},
  crossref  = {DBLP:conf/oopsla/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/oopsla/2012,
  editor    = {Gary T. Leavens and
               Matthew B. Dwyer},
  title     = {Proceedings of the 27th Annual {ACM SIGPLAN} Conference on
               Object-Oriented Programming, Systems, Languages, and Applications,
               {OOPSLA} 2012, part of {SPLASH} 2012, Tucson, AZ, USA, October
               21-25, 2012},
  booktitle = {OOPSLA},
  publisher = {ACM},
  year      = {2012},
  isbn      = {978-1-4503-1561-6},
  ee        = {http://dl.acm.org/citation.cfm?id=2384616},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Misc{RL,
  author = 	 {Grigore Ro\c{s}u and Dorel Lucanu},
  title = 	 {Circular Behavioural Reasoning},
  howpublished = {Draft Document},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@inproceedings{rosu-stefanescu-2011-nier-icse,
title = {Matching {Logic}: {A} {New} {Program} {Verification} {Approach} ({NIER} {Track})},
author = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu},
booktitle = {ICSE'11: Proceedings of the 30th International Conference on Software Engineering},
year = {2011},
pages = {868--871},
ee = {http://doi.acm.org/10.1145/1985793.1985928},
doi = {doi:10.1145/1985793.1985928},
publisher = {ACM},
isbn = {978-1-4503-0445-0},
}

@inproceedings{CadarGKPSTV11,
  author    = {Cristian Cadar and
               Patrice Godefroid and
               Sarfraz Khurshid and
               Corina S. P{\u a}s{\u a}reanu and
               Koushik Sen and
               Nikolai Tillmann and
               Willem Visser},
  title     = {Symbolic execution for software testing in practice: preliminary
               assessment},
  editor    = {Richard N. Taylor and
               Harald Gall and
               Nenad Medvidovic},
  booktitle = {ICSE},
  year      = {2011},
  pages     = {1066-1071},
  publisher = {ACM},
  ee        = {http://doi.acm.org/10.1145/1985793.1985995}
}

@article{King76,
  author    = {James C. King},
  title     = {Symbolic Execution and Program Testing},
  journal   = {Commun. ACM},
  volume    = {19},
  number    = {7},
  year      = {1976},
  pages     = {385-394},
  ee        = {http://doi.acm.org/10.1145/360248.360252},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Plotkin70,
  author = {Plotkin, Gordon D.},
  journal = {Machine Intelligence},
  pages = {153--163},
  title = {A Note on Inductive Generalization},
  volume = 5,
  year = 1970
}

@article{AlpuenteEMO09,
  author    = {Mar\'{\i}a Alpuente and
               Santiago Escobar and
               Jos{\'e} Meseguer and
               Pedro Ojeda},
  title     = {Order-Sorted Generalization},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {246},
  year      = {2009},
  pages     = {27-38},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2009.07.013}
}


@article{DBLP:journals/cacm/King76,
  author    = {James C. King},
  title     = {Symbolic Execution and Program Testing},
  journal   = {Commun. ACM},
  volume    = {19},
  number    = {7},
  year      = {1976},
  pages     = {385-394},
  ee        = {http://doi.acm.org/10.1145/360248.360252},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/icse/CadarGKPSTV11,
  author    = {Cristian Cadar and
               Patrice Godefroid and
               Sarfraz Khurshid and
               Corina S. P{\u a}s{\u }areanu and
               Koushik Sen and
               Nikolai Tillmann and
               Willem Visser},
  title     = {Symbolic execution for software testing in practice: preliminary
               assessment},
  booktitle = {ICSE},
  year      = {2011},
  pages     = {1066-1071},
  ee        = {http://doi.acm.org/10.1145/1985793.1985995},
  crossref  = {DBLP:conf/icse/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icse/2011,
  editor    = {Richard N. Taylor and
               Harald Gall and
               Nenad Medvidovic},
  title     = {Proceedings of the 33rd International Conference on Software
               Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May
               21-28, 2011},
  booktitle = {ICSE},
  publisher = {ACM},
  year      = {2011},
  isbn      = {978-1-4503-0445-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/sttt/PasareanuV09,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {A survey of new trends in symbolic execution for software
               testing and analysis},
  journal   = {STTT},
  volume    = {11},
  number    = {4},
  year      = {2009},
  pages     = {339-353},
  ee        = {http://dx.doi.org/10.1007/s10009-009-0118-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/kbse/PasareanuR10,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Neha Rungta},
  title     = {Symbolic PathFinder: symbolic execution of {Java} bytecode},
  booktitle = {ASE},
  year      = {2010},
  pages     = {179-180},
  ee        = {http://doi.acm.org/10.1145/1858996.1859035}
}

@inproceedings{DBLP:conf/issta/VisserPK04,
  author    = {Willem Visser and
               Corina S. P{\u a}s{\u a}reanu and
               Sarfraz Khurshid},
  title     = {Test input generation with {J}ava {PathFinder}},
  booktitle = {ISSTA},
  year      = {2004},
  pages     = {97-107},
  ee        = {http://doi.acm.org/10.1145/1007512.1007526},
  crossref  = {DBLP:conf/issta/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2004,
  editor    = {George S. Avrunin and
               Gregg Rothermel},
  title     = {Proceedings of the {ACM/SIGSOFT} International Symposium on
               Software Testing and Analysis, {ISSTA} 2004, {B}oston, {M}assachusetts,
               {USA}, July 11-14, 2004},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2004},
  isbn      = {1-58113-820-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@proceedings{DBLP:conf/kbse/2010,
  editor    = {Charles Pecheur and
               Jamie Andrews and
               Elisabetta Di Nitto},
  title     = {ASE 2010, 25th IEEE/ACM International Conference on Automated
               Software Engineering,  Antwerp, Belgium, September 20-24,
               2010},
  booktitle = {ASE},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-4503-0116-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@MISC{pex,
   title  = {{Pex}: Automated exploratory testing for {.NET}},
   url         ={\texttt{http://research.microsoft.com/en-us/projects/pex}},
   note     ={\\ \texttt{http://research.microsoft.com/en-us/projects/pex}}
   }
   
 @inproceedings{HalleuxT08,
  author    = {Jonathan de Halleux and
               Nikolai Tillmann},
  title     = {Parameterized Unit Testing with {Pex}},
  booktitle = {TAP},
  year      = {2008},
  pages     = {171-181},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4966},
  ee        = {http://dx.doi.org/10.1007/978-3-540-79124-9_12},
  }

   

@inproceedings{Godefroid:2005:DDA:1065010.1065036,
  author    = {Patrice Godefroid and
               Nils Klarlund and
               Koushik Sen},
  title     = {{DART}: directed automated random testing},
  booktitle = {PLDI},
  year      = {2005},
  pages     = {213-223},
  ee        = {http://doi.acm.org/10.1145/1065010.1065036},
  crossref  = {DBLP:conf/pldi/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/pldi/2005,
  editor    = {Vivek Sarkar and
               Mary W. Hall},
  title     = {Proceedings of the {ACM SIGPLAN} 2005 Conference on Programming
               Language Design and Implementation, Chicago, IL, USA, June
               12-15, 2005},
  booktitle = {PLDI},
  publisher = {ACM},
  year      = {2005},
  isbn      = {1-59593-056-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Sen:2005:CCU:1081706.1081750,
 author = {Sen, Koushik and Marinov, Darko and Agha, Gul},
 title = {{CUTE}: a concolic unit testing engine for {C}},
 booktitle = {Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering},
 series = {ESEC/FSE-13},
 year = {2005},
 isbn = {1-59593-014-0},
 location = {Lisbon, Portugal},
 pages = {263--272},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/1081706.1081750},
 doi = {10.1145/1081706.1081750},
 acmid = {1081750},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {concolic testing, data structure testing, explicit path model-checking, random testing, testing {C} programs, unit testing},
}

@inproceedings{DBLP:conf/aplas/BerdineCO05,
  author    = {Josh Berdine and
               Cristiano Calcagno and
               Peter W. O'Hearn},
  title     = {Symbolic Execution with Separation Logic},
  booktitle = {APLAS},
  year      = {2005},
  pages     = {52-68},
  ee        = {http://dx.doi.org/10.1007/11575467_5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/aplas/2005,
  editor    = {Kwangkeun Yi},
  title     = {Programming Languages and Systems, Third Asian Symposium,
               APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings},
  booktitle = {APLAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3780},
  year      = {2005},
  isbn      = {3-540-29735-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Cadar06exe:automatically,
  author    = {Cristian Cadar and
               Vijay Ganesh and
               Peter M. Pawlowski and
               David L. Dill and
               Dawson R. Engler},
  title     = {{EXE}: automatically generating inputs of death},
  booktitle = {ACM Conference on Computer and Communications Security},
  year      = {2006},
  pages     = {322-335},
  ee        = {http://doi.acm.org/10.1145/1180405.1180445},
  crossref  = {DBLP:conf/ccs/2006usa},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}
@proceedings{DBLP:conf/ccs/2006usa,
  editor    = {Ari Juels and
               Rebecca N. Wright and
               Sabrina De Capitani di Vimercati},
  title     = {Proceedings of the 13th ACM Conference on Computer and Communications
               Security, CCS 2006, Alexandria, VA, USA, Ioctober 30 - November
               3, 2006},
  booktitle = {ACM Conference on Computer and Communications Security},
  publisher = {ACM},
  year      = {2006},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}

@article{rosu-serbanuta-2010-jlap,
  title={An Overview of the {K} Semantic Framework},
  author={Grigore Ro{\c s}u and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} },
  journal={Journal of Logic and Algebraic Programming},
  volume={79},
  number={6},
  pages={397--434},
  year={2010},
  ee={http://dx.doi.org/10.1016/j.jlap.2010.03.012},
  doi={10.1016/j.jlap.2010.03.012},
}


@inproceedings{klover,
  author    = {Guodong Li and
               Indradeep Ghosh and
               Sreeranga P. Rajan},
  title     = {{KLOVER}: A Symbolic Execution and Automatic Test Generation
               Tool for {C++} Programs},
  booktitle = {CAV},
  year      = {2011},
  pages     = {609-615},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1_49},
  crossref  = {DBLP:conf/cav/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/2011,
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  title     = {Computer Aided Verification - 23rd International Conference,
               CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6806},
  year      = {2011},
  isbn      = {978-3-642-22109-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Khurshid03generalizedsymbolic,
  author    = {Sarfraz Khurshid and
               Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {Generalized Symbolic Execution for Model Checking and Testing},
  booktitle = {TACAS},
  year      = {2003},
  pages     = {553-568},
  ee        = {http://dx.doi.org/10.1007/3-540-36577-X_40},
  crossref  = {DBLP:conf/tacas/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2003,
  editor    = {Hubert Garavel and
               John Hatcliff},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 9th International Conference, {TACAS} 2003, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, {ETAPS} 2003, {Warsaw}, {Poland}, {April}
               7-11, 2003, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2619},
  year      = {2003},
  isbn      = {3-540-00898-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{Dillon:1990:VGS:78617.78622,
 author = {Dillon, Laura K.},
 title = {Verifying General Safety Properties of {Ada} Tasking Programs},
 journal = {IEEE Trans. Softw. Eng.},
 issue_date = {January 1990},
 volume = {16},
 number = {1},
 month = jan,
 year = {1990},
 issn = {0098-5589},
 pages = {51--63},
 numpages = {13},
 url = {http://dx.doi.org/10.1109/32.44363},
 doi = {10.1109/32.44363},
 acmid = {78622},
 publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 keywords = {Ada, Ada tasking programs, automating partial correctness proofs, concurrent programs, deadlock, isolation approach, multiprocessing programs, mutual exclusion, program verification., safety properties verification, symbolic execution},
}


@inproceedings{Siegel:2006:UMC:1146238.1146256,
  author    = {Stephen F. Siegel and
               Anastasia Mironova and
               George S. Avrunin and
               Lori A. Clarke},
  title     = {Using model checking with symbolic execution to verify parallel
               numerical programs},
  booktitle = {ISSTA},
  year      = {2006},
  pages     = {157-168},
  ee        = {http://doi.acm.org/10.1145/1146238.1146256},
  crossref  = {DBLP:conf/issta/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2006,
  editor    = {Lori L. Pollock and
               Mauro Pezz{\`e}},
  title     = {Proceedings of the {ACM/SIGSOFT} International Symposium on
               Software Testing and Analysis, {ISSTA} 2006, {Portland}, {Maine},
               {USA}, {J}uly 17-20, 2006},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2006},
  isbn      = {1-59593-263-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Staats:2010:PSE:1831708.1831732,
  author    = {Matt Staats and
               Corina S. P{\u a}s{\u a}reanu},
  title     = {Parallel symbolic execution for structural test generation},
  booktitle = {ISSTA},
  year      = {2010},
  pages     = {183-194},
  ee        = {http://doi.acm.org/10.1145/1831708.1831732},
  crossref  = {DBLP:conf/issta/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/issta/2010,
  editor    = {Paolo Tonella and
               Alessandro Orso},
  title     = {Proceedings of the Nineteenth International Symposium on
               Software Testing and Analysis, {ISSTA} 2010, {T}rento, {I}taly,
               {J}uly 12-16, 2010},
  booktitle = {ISSTA},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-60558-823-0},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}


@inproceedings{Pasareanu04verificationof ,
  author    = {Corina S. P{\u a}s{\u a}reanu and
               Willem Visser},
  title     = {Verification of {J}ava Programs Using Symbolic Execution and
               Invariant Generation},
  booktitle = {SPIN},
  year      = {2004},
  pages     = {164-181},
  ee        = {http://dx.doi.org/10.1007/978-3-540-24732-6_13},
  crossref  = {DBLP:conf/spin/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/spin/2004,
  editor    = {Susanne Graf and
               Laurent Mounier},
  title     = {Model Checking Software, 11th International {SPIN} Workshop,
               {Barcelona}, {Spain}, {April} 1-3, 2004, Proceedings},
  booktitle = {SPIN},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2989},
  year      = {2004},
  isbn      = {3-540-21314-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{Lee2003523,
title = {Generating test sequences using symbolic execution for event-driven real-time systems},
journal = "Microprocessors and Microsystems",
volume = "27",
number = "10",
pages = "523 - 531",
year = "2003",
note = "",
issn = "0141-9331",
doi = "10.1016/S0141-9331(03)00102-9",
url = "http://www.sciencedirect.com/science/article/pii/S0141933103001029",
author = "Nam Hee Lee and Sung Deok Cha",
keywords = "Real-time system testing",
keywords = "Symbolic execution",
keywords = "Modechart"
}


@inproceedings{schmitt07,
  author    = {Peter H. Schmitt and
               Benjamin Wei{\ss}},
  title     = {Inferring Invariants by Symbolic Execution},
  booktitle = {Proceedings of  4th International Verification Workshop (VERIFY'07)},
  year      = {2007},
  ee        = {http://ceur-ws.org/Vol-259/paper16.pdf},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/2007verify,
  editor    = {Bernhard Beckert},
  title     = {Proceedings of 4th International Verification Workshop in
               connection with {CADE}-21, {B}remen, {G}ermany, July 15-16, 2007},
  booktitle = {VERIFY},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {259},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{lucanu:hal-00744374,
    hal_id = {hal-00744374},
    url = {http://hal.inria.fr/hal-00744374},
    title = {Program Equivalence by Circular Reasoning},
    author = {Lucanu, Dorel and Rusu, Vlad},
    abstract = {We propose a deductive system for automatically proving the equivalence of programs written in deterministic languages that have a formal, term-rewriting based operational semantics. Symbolic programs (i.e., programs in which some statements or expressions are symbolic variables) can also be proved equivalent using the proposed approach. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that the deductive system is suitable for proving equivalence both for terminating and non-terminating programs. We also report on a prototype implementation of the proposed system in the $\mathbb{K}$ framework},
    language = {Anglais},
    affiliation = {Department of Computer Science , DART - INRIA Lille - Nord Europe},
    pages = {26},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-8116},
    year = {2012},
    month = Oct,
    pdf = {http://hal.inria.fr/hal-00744374/PDF/RR-8116.pdf},
}

@MISC{imponline,
   author = {Symbolic IMP},
   title={https://fmse.info.uaic.ro/tools/Symbolic-IMP/},
   url="https://fmse.info.uaic.ro/tools/Symbolic-IMP/",
   year="2012"
}
@MISC{imphoare,
   author = {Symbolic IMP},
   title={https://fmse.info.uaic.ro/tools/Symbolic-IMP/},
   url="https://fmse.info.uaic.ro/tools/Symbolic-IMP/",
   year="2012"
}
@MISC{impreachability,
   author = {Symbolic IMP},
   title={https://fmse.info.uaic.ro/tools/Symbolic-IMP/},
   url="https://fmse.info.uaic.ro/tools/Symbolic-IMP/",
   year="2012"
}

@article{DBLP:journals/cacm/Hoare69,
  author    = {C. A. R. Hoare},
  title     = {An Axiomatic Basis for Computer Programming},
  journal   = {Commun. ACM},
  volume    = {12},
  number    = {10},
  year      = {1969},
  pages     = {576-580},
  ee        = {http://doi.acm.org/10.1145/363235.363259},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-stefanescu-2012-fm,
  author    = {Grigore Rosu and Andrei Stefanescu},
  title     = {From {H}oare {L}ogic to {M}atching {L}ogic {R}eachability},
  booktitle = {Proceedings of the 18th International Symposium on Formal Methods (FM'12)},
  year      = {2012},
  pages     = {387-402},
  series    = {Lecture Notes in Computer Science},
  volume    = {7436},
  publisher = {Springer},
}


@inproceedings{DBLP:conf/fm/LazarASEMLR12,
  author    = {David Lazar and
               Andrei Arusoaie and
               Traian-Florin Serbanuta and
               Chucky Ellison and
               Radu Mereuta and
               Dorel Lucanu and
               Grigore Rosu},
  title     = {Executing Formal Semantics with the K Tool},
  booktitle = {FM},
  year      = {2012},
  pages     = {267-271},
  ee        = {http://dx.doi.org/10.1007/978-3-642-32759-9_23},
  crossref  = {DBLP:conf/fm/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fm/2012,
  editor    = {Dimitra Giannakopoulou and
               Dominique M{\'e}ry},
  title     = {FM 2012: Formal Methods - 18th International Symposium,
               Paris, France, August 27-31, 2012. Proceedings},
  booktitle = {FM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7436},
  year      = {2012},
  isbn      = {978-3-642-32758-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-32759-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{k-primer-2012-v25,
  author = {Traian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu},
  title = {The {K} Primer (version 2.5)},
  editor = {Mark Hills},
  booktitle = {K'11},
  series = {Electronic Notes in Theoretical Computer Science},
  year = {to appear},
}

@inproceedings{McCarthy,
    author = {John McCarthy},
    booktitle = {Computer Programming and Formal Systems},
    editor = {Braffort, P. and Hirschberg, D.},
    keywords = {computation},
    pages = {33--70},
    publisher = {North-Holland, Amsterdam},
    title = {{A Basis for a Mathematical Theory of Computation}},
    year = {1963}
}

@inproceedings{DBLP:dblp_journals/entcs/ArmandoBM06,
   author              = {Alessandro Armando and 
                          Massimo Benerecetti and 
                          Jacopo Mantovani},
   title               = {Model Checking Linear Programs with Arrays.},
   journal             = {Electr. Notes Theor. Comput. Sci.},
   year                = {2006},
   pages               = {79-94},
   ee                  = {http://dx.doi.org/10.1016/j.entcs.2006.01.006},
}

@inproceedings{LucanuSR2012,
author = {Dorel Lucanu and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} and Grigore Ro{\c s}u}, 
title = {The  {K} {Framework} Distilled}, 
booktitle = {9th International Workshop on Rewriting Logic and its Applications}, 
series = {Lecture Notes in Computer Science}, 
pages = {31-53}, 
year = {2012}, 
volume = {7571}, 
publisher = {Springer}, 
note = {Invited talk.}, 
}

@INPROCEEDINGS{ITS, 
author={Goshi, K. and Wray, P. and Yong Sun}, 
booktitle={Computational Intelligence and Multimedia Applications, 2001. ICCIMA 2001. Proceedings. Fourth International Conference on}, 
title={An intelligent tutoring system for teaching and learning {H}oare logic}, 
year={2001}, 
pages={293-297}, 
keywords={formal logic;intelligent tutoring systems;Hoare logic learning;intelligent tutoring system;teaching;Computer science;Education;Intelligent systems;Java;Logic;Mathematics;Rain;Sun;Tellurium;World Wide Web}, 
doi={10.1109/ICCIMA.2001.970482},}

@Misc{JAlgo,
  author = 	 {J-Algo},
  title = 	 {The Algorithm Visualization Tool},
  url = {http://j-algo.binaervarianz.de/},
  year = {2007},
  OPTmonth = 	 {},
  OPTyear = 	 {2007},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@inproceedings{Key-Hoare,
 author = {Gabrisch, Werner and Zimmermann, Wolf},
 title = {A {H}oare-style verification calculus for control state {ASM}s},
 booktitle = {Proceedings of the Fifth Balkan Conference in Informatics},
 series = {BCI '12},
 year = {2012},
 isbn = {978-1-4503-1240-0},
 location = {Novi Sad, Serbia},
 pages = {205--210},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/2371316.2371357},
 doi = {10.1145/2371316.2371357},
 acmid = {2371357},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Hoare-calculus, abstract state machines},
}


%% hal-00766220, version 2
%% http://hal.inria.fr/hal-00766220
@techreport{arusoaie:hal-00766220,
    hal_id = {hal-00766220},
    url = {http://hal.inria.fr/hal-00766220},
    title = {{A Generic Approach to Symbolic Execution}},
    author = {Arusoaie, Andrei and Lucanu, Dorel and Rusu, Vlad},
    abstract = {{We propose a generic, language-independent symbolic execution approach for languages endowed with a formal operational semantics based on term rewriting. Starting from the definition of a language $\cal L$, a new definition ${\cal L}^{\it sym}$ is automatically generated, which has the same syntax, but whose semantics extends ${\cal L}$'s data domains with symbolic values and adapts the semantical rules of $\cal L$ to deal with the new domains. Then, the symbolic execution of ${\cal L}$ programs is the concrete execution of the corresponding ${\cal L}^{\it sym}$ programs, i.e., the application of the rewrite rules in the semantics of ${\cal L}^{\it sym}$. We prove that the symbolic execution thus defined has the adequate properties normally expected from it, and illustrate the approach on a simple imperative language defined in the $\mathbb{\K}$ framework. A prototype symbolic execution engine also written in $\mathbb{\K}$ is presented.}},
    keywords = {Symbolic Execution, Term Rewriting, $\mathbb{\K}$ framework},
    language = {Anglais},
    affiliation = {Department of Compter Science , Department of Computer Science , DART - INRIA Lille - Nord Europe},
    pages = {21},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-8189},
    year = {2012},
    month = Dec,
    pdf = {http://hal.inria.fr/hal-00766220/PDF/symbexec-techreport.pdf},
}


@article{Sasse:2007:JVT:1279349.1279449,
 author = {Sasse, Ralf and Meseguer, Jos{\'e}},
 title = {{Java+ITP}: A Verification Tool Based on {H}oare {L}ogic and {A}lgebraic {S}emantics},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {July, 2007},
 volume = {176},
 number = {4},
 month = jul,
 year = {2007},
 issn = {1571-0661},
 pages = {29--46},
 numpages = {18},
 url = {http://dx.doi.org/10.1016/j.entcs.2007.06.006},
 doi = {10.1016/j.entcs.2007.06.006},
 acmid = {1279449},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Hoare logic, Java, algebraic semantics, program verification},
} 

@inproceedings{DBLP:conf/arith/BoldoF07,
  author    = {Sylvie Boldo and
               Jean-Christophe Filli{\^a}tre},
  title     = {Formal Verification of Floating-Point Programs},
  booktitle = {IEEE Symposium on Computer Arithmetic},
  year      = {2007},
  pages     = {187-194},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ARITH.2007.20},
  crossref  = {DBLP:conf/arith/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/arith/2007,
  title     = {18th IEEE Symposium on Computer Arithmetic (ARITH-18 2007),
               25-27 June 2007, Montpellier, France},
  booktitle = {IEEE Symposium on Computer Arithmetic},
  publisher = {IEEE Computer Society},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{lazar-arusoaie-serbanuta-ellison-mereuta-lucanu-rosu-2012-fm,
author={David Lazar and Andrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Radu Mereuta and Dorel Lucanu and Grigore Ro\c{s}u},
title={Executing Formal Semantics with the {K} Tool},
year={2012},
publisher={Springer},
booktitle={FM},
series={LNCS},
volume={7436},
pages={267-271},
ee={http://dx.doi.org/10.1007/978-3-642-32759-9_23},
}


@book{DBLP:books/ph/Dijkstra76,
  author    = {Edsger W. Dijkstra},
  title     = {A Discipline of Programming},
  publisher = {Prentice-Hall},
  year      = {1976},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@incollection{Gordon10,
    abstract = {Hoare's celebrated paper entitled  ” An Axiomatic Basis for Computer Programming” appeared in 1969, so the Hoare formula P { S } Q is now 40 years old! That paper introduced Hoare Logic, which is still the basis for program verification today, but is now mechanised inside sophisticated verification systems. We aim here to give an accessible introduction to methods for proving Hoare formulae based both on the forward computation of postconditions and on the backward computation of preconditions. Although precondition methods are better known, computing postconditions provides a verification framework that encompasses methods ranging from symbolic execution to full deductive proof of correctness.},
    address = {London},
    author = {Gordon, Mike and Collavizza, H\'{e}l\`{e}ne},
    booktitle = {Reflections on the Work of C.A.R. Hoare},
    chapter = {5},
    citeulike-article-id = {9758745},
    citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-1-84882-912-1\_5},
    citeulike-linkout-1 = {http://www.springerlink.com/content/t62u113075345m45},
    doi = {10.1007/978-1-84882-912-1\_5},
    editor = {Roscoe, A. W. and Jones, Cliff B. and Wood, Kenneth R.},
    isbn = {978-1-84882-911-4},
    keywords = {2011, hoare-logic, strongest-postcondition, weakest-precondition},
    pages = {101--121},
    posted-at = {2011-09-12 15:16:21},
    priority = {2},
    publisher = {Springer London},
    series = {History of Computing},
    title = {{Forward with Hoare}},
    url = {http://dx.doi.org/10.1007/978-1-84882-912-1\_5},
    year = {2010}
}

@INPROCEEDINGS{Saabas05acompositional,
    author = {Ando Saabas and Tarmo Uustalu},
    title = {A compositional natural semantics and {H}oare logic for low-level languages},
    booktitle = {In: Proceedings of the Second Workshop on Structured Operational Semantics},
    year = {2005},
    pages = {151--168},
    publisher = {Elsevier}
}

@inproceedings{DBLP:conf/lics/Reynolds02,
  author    = {John C. Reynolds},
  title     = {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle = {LICS},
  year      = {2002},
  pages     = {55-74},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029817},
  crossref  = {DBLP:conf/lics/2002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/lics/2002,
  title     = {17th IEEE Symposium on Logic in Computer Science (LICS 2002),
               22-25 July 2002, Copenhagen, Denmark, Proceedings},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year      = {2002},
  isbn      = {0-7695-1483-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{FLOYD67,
  AUTHOR = {Floyd, Robert W.},
  TITLE = {Assigning Meanings to Programs},
  BOOKTITLE = {Mathematical Aspects of Computer Science},
  PLACE = {New York City},
  DATES = {April 5--7, 1966},
  EDITOR = {J. T. Schwartz},
  SERIES = {Proceedings of Symposia in Applied Mathematics},
  VOLUME = {19},
  PUBLISHER = {American Mathematical Society},
  ADDRESS = {Providence, Rhode Island},
  YEAR = {1967},
  PAGES = {19--32},
  CHECKED = {13 September 1992}
}

@inproceedings{Barnett:2004:SPS:2131546.2131549,
 author = {Barnett, Mike and Leino, K. Rustan M. and Schulte, Wolfram},
 title = {The {S}pec\# programming system: an overview},
 booktitle = {Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices},
 series = {CASSIS'04},
 year = {2005},
 isbn = {3-540-24287-2, 978-3-540-24287-1},
 location = {Marseille, France},
 pages = {49--69},
 numpages = {21},
 url = {http://dx.doi.org/10.1007/978-3-540-30569-9_3},
 doi = {10.1007/978-3-540-30569-9_3},
 acmid = {2131549},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 